0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 89 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 21 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 4 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 PiDPToQDPProof (⇒, 0 ms)
↳23 QDP
↳24 Rewriting (⇔, 0 ms)
↳25 QDP
↳26 UsableRulesProof (⇔, 0 ms)
↳27 QDP
↳28 QReductionProof (⇔, 3 ms)
↳29 QDP
↳30 Rewriting (⇔, 0 ms)
↳31 QDP
↳32 UsableRulesProof (⇔, 0 ms)
↳33 QDP
↳34 QReductionProof (⇔, 0 ms)
↳35 QDP
↳36 Instantiation (⇔, 0 ms)
↳37 QDP
↳38 QDPOrderProof (⇔, 118 ms)
↳39 QDP
↳40 DependencyGraphProof (⇔, 0 ms)
↳41 TRUE
PERMA_IN_GA(cons(X1, X2), cons(X1, X3)) → U3_GA(X1, X2, X3, ap2cB_in_ga(X2, X4))
U3_GA(X1, X2, X3, ap2cB_out_ga(X2, X4)) → U4_GA(X1, X2, X3, permA_in_ga(X4, X3))
U3_GA(X1, X2, X3, ap2cB_out_ga(X2, X4)) → PERMA_IN_GA(X4, X3)
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → U5_GA(X1, X2, X3, X4, ap1C_in_aaag(X5, X3, X6, X2))
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → AP1C_IN_AAAG(X5, X3, X6, X2)
AP1C_IN_AAAG(cons(X1, X2), X3, X4, cons(X1, X5)) → U1_AAAG(X1, X2, X3, X4, X5, ap1C_in_aaag(X2, X3, X4, X5))
AP1C_IN_AAAG(cons(X1, X2), X3, X4, cons(X1, X5)) → AP1C_IN_AAAG(X2, X3, X4, X5)
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → U6_GA(X1, X2, X3, X4, ap1cC_in_aaag(X5, X3, X6, X2))
U6_GA(X1, X2, X3, X4, ap1cC_out_aaag(X5, X3, X6, X2)) → U7_GA(X1, X2, X3, X4, ap2E_in_gga(X5, X6, X7))
U6_GA(X1, X2, X3, X4, ap1cC_out_aaag(X5, X3, X6, X2)) → AP2E_IN_GGA(X5, X6, X7)
AP2E_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → U2_GGA(X1, X2, X3, X4, ap2E_in_gga(X2, X3, X4))
AP2E_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → AP2E_IN_GGA(X2, X3, X4)
U6_GA(X1, X2, X3, X4, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, X3, X4, ap2cD_in_ggga(X1, X5, X6, X7))
U8_GA(X1, X2, X3, X4, ap2cD_out_ggga(X1, X5, X6, X7)) → U9_GA(X1, X2, X3, X4, permA_in_ga(X7, X4))
U8_GA(X1, X2, X3, X4, ap2cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7, X4)
ap2cB_in_ga(X1, X1) → ap2cB_out_ga(X1, X1)
ap1cC_in_aaag(nil, X1, X2, cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X2), X3, X4, cons(X1, X5)) → U16_aaag(X1, X2, X3, X4, X5, ap1cC_in_aaag(X2, X3, X4, X5))
U16_aaag(X1, X2, X3, X4, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap2cD_in_ggga(X1, X2, X3, cons(X1, X4)) → U18_ggga(X1, X2, X3, X4, ap2cE_in_gga(X2, X3, X4))
ap2cE_in_gga(nil, X1, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U17_gga(X1, X2, X3, X4, ap2cE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, X4, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
PERMA_IN_GA(cons(X1, X2), cons(X1, X3)) → U3_GA(X1, X2, X3, ap2cB_in_ga(X2, X4))
U3_GA(X1, X2, X3, ap2cB_out_ga(X2, X4)) → U4_GA(X1, X2, X3, permA_in_ga(X4, X3))
U3_GA(X1, X2, X3, ap2cB_out_ga(X2, X4)) → PERMA_IN_GA(X4, X3)
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → U5_GA(X1, X2, X3, X4, ap1C_in_aaag(X5, X3, X6, X2))
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → AP1C_IN_AAAG(X5, X3, X6, X2)
AP1C_IN_AAAG(cons(X1, X2), X3, X4, cons(X1, X5)) → U1_AAAG(X1, X2, X3, X4, X5, ap1C_in_aaag(X2, X3, X4, X5))
AP1C_IN_AAAG(cons(X1, X2), X3, X4, cons(X1, X5)) → AP1C_IN_AAAG(X2, X3, X4, X5)
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → U6_GA(X1, X2, X3, X4, ap1cC_in_aaag(X5, X3, X6, X2))
U6_GA(X1, X2, X3, X4, ap1cC_out_aaag(X5, X3, X6, X2)) → U7_GA(X1, X2, X3, X4, ap2E_in_gga(X5, X6, X7))
U6_GA(X1, X2, X3, X4, ap1cC_out_aaag(X5, X3, X6, X2)) → AP2E_IN_GGA(X5, X6, X7)
AP2E_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → U2_GGA(X1, X2, X3, X4, ap2E_in_gga(X2, X3, X4))
AP2E_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → AP2E_IN_GGA(X2, X3, X4)
U6_GA(X1, X2, X3, X4, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, X3, X4, ap2cD_in_ggga(X1, X5, X6, X7))
U8_GA(X1, X2, X3, X4, ap2cD_out_ggga(X1, X5, X6, X7)) → U9_GA(X1, X2, X3, X4, permA_in_ga(X7, X4))
U8_GA(X1, X2, X3, X4, ap2cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7, X4)
ap2cB_in_ga(X1, X1) → ap2cB_out_ga(X1, X1)
ap1cC_in_aaag(nil, X1, X2, cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X2), X3, X4, cons(X1, X5)) → U16_aaag(X1, X2, X3, X4, X5, ap1cC_in_aaag(X2, X3, X4, X5))
U16_aaag(X1, X2, X3, X4, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap2cD_in_ggga(X1, X2, X3, cons(X1, X4)) → U18_ggga(X1, X2, X3, X4, ap2cE_in_gga(X2, X3, X4))
ap2cE_in_gga(nil, X1, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U17_gga(X1, X2, X3, X4, ap2cE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, X4, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
AP2E_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → AP2E_IN_GGA(X2, X3, X4)
ap2cB_in_ga(X1, X1) → ap2cB_out_ga(X1, X1)
ap1cC_in_aaag(nil, X1, X2, cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X2), X3, X4, cons(X1, X5)) → U16_aaag(X1, X2, X3, X4, X5, ap1cC_in_aaag(X2, X3, X4, X5))
U16_aaag(X1, X2, X3, X4, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap2cD_in_ggga(X1, X2, X3, cons(X1, X4)) → U18_ggga(X1, X2, X3, X4, ap2cE_in_gga(X2, X3, X4))
ap2cE_in_gga(nil, X1, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U17_gga(X1, X2, X3, X4, ap2cE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, X4, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
AP2E_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → AP2E_IN_GGA(X2, X3, X4)
AP2E_IN_GGA(cons(X1, X2), X3) → AP2E_IN_GGA(X2, X3)
From the DPs we obtained the following set of size-change graphs:
AP1C_IN_AAAG(cons(X1, X2), X3, X4, cons(X1, X5)) → AP1C_IN_AAAG(X2, X3, X4, X5)
ap2cB_in_ga(X1, X1) → ap2cB_out_ga(X1, X1)
ap1cC_in_aaag(nil, X1, X2, cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X2), X3, X4, cons(X1, X5)) → U16_aaag(X1, X2, X3, X4, X5, ap1cC_in_aaag(X2, X3, X4, X5))
U16_aaag(X1, X2, X3, X4, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap2cD_in_ggga(X1, X2, X3, cons(X1, X4)) → U18_ggga(X1, X2, X3, X4, ap2cE_in_gga(X2, X3, X4))
ap2cE_in_gga(nil, X1, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U17_gga(X1, X2, X3, X4, ap2cE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, X4, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
AP1C_IN_AAAG(cons(X1, X2), X3, X4, cons(X1, X5)) → AP1C_IN_AAAG(X2, X3, X4, X5)
AP1C_IN_AAAG(cons(X1, X5)) → AP1C_IN_AAAG(X5)
From the DPs we obtained the following set of size-change graphs:
U3_GA(X1, X2, X3, ap2cB_out_ga(X2, X4)) → PERMA_IN_GA(X4, X3)
PERMA_IN_GA(cons(X1, X2), cons(X1, X3)) → U3_GA(X1, X2, X3, ap2cB_in_ga(X2, X4))
PERMA_IN_GA(cons(X1, X2), cons(X3, X4)) → U6_GA(X1, X2, X3, X4, ap1cC_in_aaag(X5, X3, X6, X2))
U6_GA(X1, X2, X3, X4, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, X3, X4, ap2cD_in_ggga(X1, X5, X6, X7))
U8_GA(X1, X2, X3, X4, ap2cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7, X4)
ap2cB_in_ga(X1, X1) → ap2cB_out_ga(X1, X1)
ap1cC_in_aaag(nil, X1, X2, cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X2), X3, X4, cons(X1, X5)) → U16_aaag(X1, X2, X3, X4, X5, ap1cC_in_aaag(X2, X3, X4, X5))
U16_aaag(X1, X2, X3, X4, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap2cD_in_ggga(X1, X2, X3, cons(X1, X4)) → U18_ggga(X1, X2, X3, X4, ap2cE_in_gga(X2, X3, X4))
ap2cE_in_gga(nil, X1, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U17_gga(X1, X2, X3, X4, ap2cE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, X4, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
U3_GA(X1, X2, ap2cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, ap2cB_in_ga(X2))
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, ap1cC_in_aaag(X2))
U6_GA(X1, X2, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, ap2cD_in_ggga(X1, X5, X6))
U8_GA(X1, X2, ap2cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
ap2cB_in_ga(X1) → ap2cB_out_ga(X1, X1)
ap1cC_in_aaag(cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X5)) → U16_aaag(X1, X5, ap1cC_in_aaag(X5))
U16_aaag(X1, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap2cD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, ap2cE_in_gga(X2, X3))
ap2cE_in_gga(nil, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, ap2cE_in_gga(X2, X3))
U17_gga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
ap2cB_in_ga(x0)
ap1cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
ap2cD_in_ggga(x0, x1, x2)
ap2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, ap2cB_out_ga(X2, X2))
U3_GA(X1, X2, ap2cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, ap1cC_in_aaag(X2))
U6_GA(X1, X2, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, ap2cD_in_ggga(X1, X5, X6))
U8_GA(X1, X2, ap2cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, ap2cB_out_ga(X2, X2))
ap2cB_in_ga(X1) → ap2cB_out_ga(X1, X1)
ap1cC_in_aaag(cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X5)) → U16_aaag(X1, X5, ap1cC_in_aaag(X5))
U16_aaag(X1, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap2cD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, ap2cE_in_gga(X2, X3))
ap2cE_in_gga(nil, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, ap2cE_in_gga(X2, X3))
U17_gga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U18_ggga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
ap2cB_in_ga(x0)
ap1cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
ap2cD_in_ggga(x0, x1, x2)
ap2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U3_GA(X1, X2, ap2cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, ap1cC_in_aaag(X2))
U6_GA(X1, X2, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, ap2cD_in_ggga(X1, X5, X6))
U8_GA(X1, X2, ap2cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, ap2cB_out_ga(X2, X2))
ap2cD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, ap2cE_in_gga(X2, X3))
ap2cE_in_gga(nil, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, ap2cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
ap1cC_in_aaag(cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X5)) → U16_aaag(X1, X5, ap1cC_in_aaag(X5))
U16_aaag(X1, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap2cB_in_ga(x0)
ap1cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
ap2cD_in_ggga(x0, x1, x2)
ap2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
ap2cB_in_ga(x0)
U3_GA(X1, X2, ap2cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, ap1cC_in_aaag(X2))
U6_GA(X1, X2, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, ap2cD_in_ggga(X1, X5, X6))
U8_GA(X1, X2, ap2cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, ap2cB_out_ga(X2, X2))
ap2cD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, ap2cE_in_gga(X2, X3))
ap2cE_in_gga(nil, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, ap2cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
ap1cC_in_aaag(cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X5)) → U16_aaag(X1, X5, ap1cC_in_aaag(X5))
U16_aaag(X1, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap1cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
ap2cD_in_ggga(x0, x1, x2)
ap2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U6_GA(X1, X2, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, ap2cE_in_gga(X5, X6)))
U3_GA(X1, X2, ap2cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, ap1cC_in_aaag(X2))
U8_GA(X1, X2, ap2cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, ap2cB_out_ga(X2, X2))
U6_GA(X1, X2, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, ap2cE_in_gga(X5, X6)))
ap2cD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, ap2cE_in_gga(X2, X3))
ap2cE_in_gga(nil, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, ap2cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
ap1cC_in_aaag(cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X5)) → U16_aaag(X1, X5, ap1cC_in_aaag(X5))
U16_aaag(X1, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap1cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
ap2cD_in_ggga(x0, x1, x2)
ap2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U3_GA(X1, X2, ap2cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, ap1cC_in_aaag(X2))
U8_GA(X1, X2, ap2cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, ap2cB_out_ga(X2, X2))
U6_GA(X1, X2, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, ap2cE_in_gga(X5, X6)))
ap2cE_in_gga(nil, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, ap2cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
ap1cC_in_aaag(cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X5)) → U16_aaag(X1, X5, ap1cC_in_aaag(X5))
U16_aaag(X1, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap1cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
ap2cD_in_ggga(x0, x1, x2)
ap2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
ap2cD_in_ggga(x0, x1, x2)
U3_GA(X1, X2, ap2cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, ap1cC_in_aaag(X2))
U8_GA(X1, X2, ap2cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, ap2cB_out_ga(X2, X2))
U6_GA(X1, X2, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, ap2cE_in_gga(X5, X6)))
ap2cE_in_gga(nil, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, ap2cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
ap1cC_in_aaag(cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X5)) → U16_aaag(X1, X5, ap1cC_in_aaag(X5))
U16_aaag(X1, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap1cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
ap2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U3_GA(z0, z1, ap2cB_out_ga(z1, z1)) → PERMA_IN_GA(z1)
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, ap1cC_in_aaag(X2))
U8_GA(X1, X2, ap2cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, ap2cB_out_ga(X2, X2))
U6_GA(X1, X2, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, ap2cE_in_gga(X5, X6)))
U3_GA(z0, z1, ap2cB_out_ga(z1, z1)) → PERMA_IN_GA(z1)
ap2cE_in_gga(nil, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, ap2cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
ap1cC_in_aaag(cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X5)) → U16_aaag(X1, X5, ap1cC_in_aaag(X5))
U16_aaag(X1, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap1cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
ap2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U6_GA(X1, X2, ap1cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, ap2cE_in_gga(X5, X6)))
U3_GA(z0, z1, ap2cB_out_ga(z1, z1)) → PERMA_IN_GA(z1)
POL(PERMA_IN_GA(x1)) = x1
POL(U16_aaag(x1, x2, x3)) = 1 + x3
POL(U17_gga(x1, x2, x3, x4)) = 1 + x4
POL(U18_ggga(x1, x2, x3, x4)) = x4
POL(U3_GA(x1, x2, x3)) = x2 + x3
POL(U6_GA(x1, x2, x3)) = 1 + x3
POL(U8_GA(x1, x2, x3)) = x3
POL(ap1cC_in_aaag(x1)) = x1
POL(ap1cC_out_aaag(x1, x2, x3, x4)) = 1 + x1 + x3
POL(ap2cB_out_ga(x1, x2)) = 1
POL(ap2cD_out_ggga(x1, x2, x3, x4)) = x4
POL(ap2cE_in_gga(x1, x2)) = 1 + x1 + x2
POL(ap2cE_out_gga(x1, x2, x3)) = 1 + x3
POL(cons(x1, x2)) = 1 + x2
POL(nil) = 0
ap1cC_in_aaag(cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X5)) → U16_aaag(X1, X5, ap1cC_in_aaag(X5))
ap2cE_in_gga(nil, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, ap2cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
U16_aaag(X1, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
PERMA_IN_GA(cons(X1, X2)) → U6_GA(X1, X2, ap1cC_in_aaag(X2))
U8_GA(X1, X2, ap2cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(cons(X1, X2)) → U3_GA(X1, X2, ap2cB_out_ga(X2, X2))
ap2cE_in_gga(nil, X1) → ap2cE_out_gga(nil, X1, X1)
ap2cE_in_gga(cons(X1, X2), X3) → U17_gga(X1, X2, X3, ap2cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cD_out_ggga(X1, X2, X3, cons(X1, X4))
U17_gga(X1, X2, X3, ap2cE_out_gga(X2, X3, X4)) → ap2cE_out_gga(cons(X1, X2), X3, cons(X1, X4))
ap1cC_in_aaag(cons(X1, X2)) → ap1cC_out_aaag(nil, X1, X2, cons(X1, X2))
ap1cC_in_aaag(cons(X1, X5)) → U16_aaag(X1, X5, ap1cC_in_aaag(X5))
U16_aaag(X1, X5, ap1cC_out_aaag(X2, X3, X4, X5)) → ap1cC_out_aaag(cons(X1, X2), X3, X4, cons(X1, X5))
ap1cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
ap2cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)